A:MsgA, l:IdLnk, k:Knd, s:A.state, v:A.da(k).
ma-frame-compat(A;A)
 A.bframe(k sends on l)
 filter(ms.mlnk(ms) = l;A.sends(k,s,v)) = nil  A.Msg List 

latex

Definitions

<a,b>, s = t, filter(P;l), M.sends(k,s,v), a = b, nil, M.Msg, M.V(k), MsgA, Valtype(da;k), ma-frame-compat(A;B), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), M.state, M.da(a), xdom(f). v=f(x)   P(x;v), State(ds), x  dom(f), product-deq(A;B;a;b), IdLnkDeq, a:A fp B(a), IdDeq, 1of(t), Top, type List, f(x)?z, KindDeq, rcv(l,tg), 2of(t), x. t(x), x.A(x), Type, Void, S  T, x:AB(x), IdLnk, Knd, x:AB(x), Id, t  T, b, P & Q, x:A. B(x), A, P  Q, False

Lemmas

IdLnk wf, Knd wf, pi2 wf, rcv wf, Kind-deq wf, fpf-cap wf, top wf, pi1 wf, id-deq wf, Id wf, fpf-trivial-subtype-top, idlnk-deq wf, product-deq wf, fpf-dom wf, assert wf, ma-da wf, subtype rel self, ma-msg wf, ma-send-val-nil, msga wf, ma-st wf, ma-frame-compat wf, ma-bframe wf, not wf